Daniel Wessel, University of Verona

A formal approach to Menger's theorem (jww Roberta Bonacina)

Menger's theorem, a classic and cornerstone result of graph theory, has seen a fair amount of proofs within the 95 years of his "Zur allgemeinen Kurventheorie". Indeed there's a story with many facets, to which yet another one can be added by a slight shift of focus: with a suitable lattice at hand, Menger's theorem reappears through the existence of enough prime ideals as counterpart to (non-)collapse. This offers further evidence for the applicability of formal methods in graph theory, as pioneered by Matiyasevich's use of resolution calculi.